package br.cin.ufpe.rabbit;

import gov.nasa.jpf.jvm.ElementInfo;
import gov.nasa.jpf.jvm.FieldInfo;
import gov.nasa.jpf.jvm.Heap;
import gov.nasa.jpf.jvm.MethodInfo;
import gov.nasa.jpf.jvm.ThreadInfo;
import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
import gov.nasa.jpf.jvm.bytecode.Instruction;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.util.Pair;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeSet;

/*********************************************
 * one object of this kind states that:
 * 
 * the access to the memory cell objRef.fi is potentially vulnerable to data
 * races. we observed that multiple threads access this cell for reading and
 * writing and additionally in at least one case they don't agree in the
 * synchronization monitor used to protect data.
 ********************************************/
public class PotentialRaceInfo {

	public static class MemoryAccess {
		public MemoryAccess(Set<ElementInfo> lockset,
				List<ThreadInfo> runningThreads) {
			this.lockSet = lockset;
			this.runningThreads = runningThreads;
		}

		public Set<ElementInfo> lockSet;
		public List<ThreadInfo> runningThreads;

	}

	/**
	 * fields
	 */
	Integer objRef;
	FieldInfo fi;
	Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>> accessMap;

	// just a flag to indicate if this potential could leave to a race
	boolean hasRace;

	/**
	 * constructor
	 * 
	 * @param objRef
	 * @param fi
	 * @param lockSets
	 */
	public PotentialRaceInfo(Integer objRef, FieldInfo fi,
			Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>> lockSets) {
		super();
		this.objRef = objRef;
		this.fi = fi;
		this.accessMap = lockSets;
	}

	@Override
	public int hashCode() {
		return objRef;
	}

	
	public void Analize(Search search) {
		
		PotentialRaceInfo Analized = this;
		// StringBuffer sb = new StringBuffer();

		Set<ElementInfo> monitors = new TreeSet<ElementInfo>(RabbitConfig.comp);
		Heap heap = search.getVM().getSystemState().getHeap();

		int id = Analized.objRef;
		String msg = null;
		

		Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>> tmap = Analized.accessMap;
		if (tmap.entrySet().size() < 2) {
			Analized.hasRace = false;
		}

		for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry1 : tmap
				.entrySet()) {
			ThreadInfo ti = entry1.getKey();
			List<Instruction> itemsToRemove = new ArrayList<Instruction>();
			for (Map.Entry<Instruction, List<MemoryAccess>> entry2 : entry1
					.getValue().entrySet()) {
				Instruction insn = entry2.getKey();
				List<MemoryAccess> set = entry2.getValue();
				boolean instructionHasAnotherThread = false;
			
				
				for (MemoryAccess mAccess : set) {
					boolean mAccesHasThread = false;
					for (ThreadInfo runningTi : mAccess.runningThreads) {
						for (ThreadInfo ti2 : tmap.keySet()) {
//							if (ti.getId() == ti2.getId()) {
//								continue;
//							} else
							if (runningTi.getId() == ti2.getId()) {
								mAccesHasThread = true;
								instructionHasAnotherThread = true;
							}
						}
					}
				}
				if (!instructionHasAnotherThread) {
					itemsToRemove.add(insn); //optimization 1
				}
			}
			for (Instruction remInsn : itemsToRemove) {
				tmap.get(ti).remove(remInsn);
			}
		}

		// return dump(search);//sb.toString();
	}

	public String dump(Search search, boolean showThreads) {
		StringBuffer sb = new StringBuffer();

		Set<ElementInfo> monitors = new TreeSet<ElementInfo>(RabbitConfig.comp);
		Heap heap = search.getVM().getSystemState().getHeap();

		int id = objRef;
		String msg = null;

		if (id == -1) {
			msg = "null reference";
		} else {
			try {
				msg = heap.get(id).getClassInfo().getName();
			} catch (NullPointerException _) {
				if (this.fi.isStatic()) {
					msg = "static field";
				} else {
					msg = objRef + "";
				}
			}
		}

		if (msg == null) {
			if (RabbitConfig.DEBUG) {
				sb.append("object id: ");
				sb.append(id);
				sb.append("(garbage collected)\n");
			}
			return sb.toString();
		}
		Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>> tmap = accessMap;
		if (tmap.entrySet().size() > 1) {

			if (!this.fi.isStatic()) {
				sb.append("object id: ");
				sb.append(id);
			}
			sb.append(" (");
			sb.append(msg);
			sb.append(")");
			sb.append("\n");

			sb.append("  field: ");
			sb.append(fi);
			sb.append("\n");

			boolean hasSimultaneousThread = false;
			for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry3 : tmap
					.entrySet()) {
				ThreadInfo ti = entry3.getKey();

				sb.append("    thread id: ");
				sb.append(ti.getId());
				sb.append(" (");
				sb.append(ti.getName());
				sb.append(")");
				sb.append("\n");

				for (Map.Entry<Instruction, List<MemoryAccess>> entry4 : entry3
						.getValue().entrySet()) {
					Instruction insn = entry4.getKey();
					int opcode = insn.getByteCode();
					String msg2 = (opcode == RabbitConfig.PUTFIELD_opcode) ? "WRITE"
							: (opcode == RabbitConfig.PUTSTATIC_opcode) ? "WRITE"
									: "READ";

					sb.append("      instruction: ");
					sb.append(insn.getSourceLocation());
					sb.append(" ");
					sb.append(msg2);
					sb.append(" ");

					sb.append(" [");
					List<MemoryAccess> set = entry4.getValue();
					for (MemoryAccess sei : set) {
						monitors.addAll(sei.lockSet);
						int i = 0, size = sei.lockSet.size();
						sb.append("(");
						for (ElementInfo ei : sei.lockSet) {
							i++;
							sb.append(ei.getIndex());
							if (i < size) {
								sb.append(", ");
							}
						}
						sb.append(")");
					}
					sb.append("] ");
					if (showThreads) {
						for (MemoryAccess sei : set) {
							// monitors.addAll(sei.runningThreads);
							int i = 0, size = sei.runningThreads.size();
							sb.append("(");
							for (ThreadInfo tin : sei.runningThreads) {
								i++;
								sb.append("thread-" + tin.getId());
								if (i < size) {
									sb.append(", ");
								}
							}
							sb.append(")");
						}
					}
					sb.append("] \n");
				}
			}

			sb.append("============================\n");
			for (ElementInfo ei : monitors) {
				sb.append("monitor id ");
				sb.append(ei.getIndex());
				sb.append(" ");
				sb.append(ei.getClassInfo().getName());
				sb.append("\n");
			}

		}
		return sb.toString();
	}

	public String toString(Search search) {
		StringBuffer sb = new StringBuffer();

		Set<ElementInfo> monitors = new TreeSet<ElementInfo>(RabbitConfig.comp);
		Heap heap = search.getVM().getSystemState().getHeap();

		int id = objRef;
		String msg = null;

		if (id == -1) {
			msg = "null reference";
		} else {
			try {
				msg = heap.get(id).getClassInfo().getName();
			} catch (NullPointerException _) {
				if (this.fi.isStatic()) {
					msg = "static field";
				}
			}
		}

		if (msg == null) {
			if (RabbitConfig.DEBUG) {
				sb.append("object id: ");
				sb.append(id);
				sb.append("(garbage collected)\n");
			}
			return sb.toString();
		}
		Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>> tmap = accessMap;
		if (tmap.entrySet().size() > 1) {

			if (!this.fi.isStatic()) {
				sb.append("object id: ");
				sb.append(id);
			}
			sb.append(" (");
			sb.append(msg);
			sb.append(")");
			sb.append("\n");

			sb.append("  field: ");
			sb.append(fi);
			sb.append("\n");

			for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry3 : tmap
					.entrySet()) {
				boolean hasSimultaneousThread = false;
				ThreadInfo ti = entry3.getKey();
				//
				// // verifies if the ti have run simultaneously with another
				// // thread Info
				// for (Map.Entry<ThreadInfo, Map<Instruction,
				// List<MemoryAccess>>> entryTI : tmap
				// .entrySet()) {
				// if (ti == entryTI.getKey()) {
				// continue;
				// }
				//
				// for (Map.Entry<Instruction, List<MemoryAccess>> entryInsn :
				// entryTI
				// .getValue().entrySet()) {
				//
				// for (MemoryAccess ma1 : entryInsn.getValue()) {
				// if (ma1.runningThreads.contains(ti)) {
				// hasSimultaneousThread = true;
				// }
				// }
				// }
				// }
				// if (!hasSimultaneousThread) {
				// continue;
				// }
				String threadString = new String();
				threadString = "    thread id: " + ti.getId() + " ("
						+ ti.getName() + ")\n";
				// sb.append("    thread id: ");
				// sb.append(ti.getId());
				// sb.append(" (");
				// sb.append(ti.getName());
				// sb.append(")");
				// sb.append("\n");
				sb.append(threadString);

				for (Map.Entry<Instruction, List<MemoryAccess>> entry4 : entry3
						.getValue().entrySet()) {

					sb.append(printMap(entry4));
					// List<MemoryAccess> set = entry4.getValue();
					// for (MemoryAccess ma : set) {
					// for (ThreadInfo taccess : ma.runningThreads) {
					// Map<Instruction, List<MemoryAccess>> simAccess = tmap
					// .get(taccess);
					// if(simAccess == null || taccess.getId() == ti.getId()){
					// //System.err.println(taccess.getName()+
					// " n�o encontrada no mapa");
					// continue;
					// }
					// sb.append("    thread id: ");
					// sb.append(taccess.getId());
					// sb.append(" (");
					// sb.append(taccess.getName());
					// sb.append(")");
					// sb.append("\n");
					//
					// for(Map.Entry<Instruction, List<MemoryAccess>> entry5 :
					// simAccess.entrySet())
					// sb.append(printMap(entry5));
					//
					// }
					// }
				}
			}

		}
		return sb.toString();
	}

	public HashSet<ThreadInfoPair> getInterestingThreads() {
		HashSet<ThreadInfoPair> result = new HashSet<ThreadInfoPair>();

		for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry1 : accessMap
				.entrySet()) {
			ThreadInfo t1 = entry1.getKey();
			for (Map.Entry<Instruction, List<MemoryAccess>> entry2 : entry1
					.getValue().entrySet()) {
				Instruction insn1 = entry2.getKey();
				if (!RabbitListener.isWrite(insn1.getByteCode()))
					continue;
				for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry3 : accessMap
						.entrySet()) {
					ThreadInfo t2 = entry3.getKey();
					if (t1.getName().equals(t2.getName()))
						continue;
					for (Map.Entry<Instruction, List<MemoryAccess>> entry4 : entry3
							.getValue().entrySet()) {
						Instruction insn2 = entry4.getKey();
						// TODO: ignoring write-write conflicts
						if (RabbitListener.isWrite(insn2.getByteCode()))
							continue;
						// check locks!
						List<MemoryAccess> writeLocks = entry2.getValue();
						List<MemoryAccess> readLocks = entry4.getValue();
						if (isUnprotected(writeLocks, readLocks)) {
							result.add(new ThreadInfoPair(t1, t2));
						}
					}
				}
			}
		}
		return result;
	}

	@SuppressWarnings({ "rawtypes", "unchecked" })
	public void updatePotentialRacesList(
			List<Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>> result) {
		// Set<ThreadInfo> visited = new TreeSet<ThreadInfo>();
		for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry1 : accessMap
				.entrySet()) {
			ThreadInfo t1 = entry1.getKey();
			// if (t1.getState() == State.TERMINATED) continue;
			for (Map.Entry<Instruction, List<MemoryAccess>> entry2 : entry1
					.getValue().entrySet()) {
				Instruction insn1 = entry2.getKey();
				if (!RabbitListener.isWrite(insn1.getByteCode()))
					continue;
				for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry3 : accessMap
						.entrySet()) {
					ThreadInfo t2 = entry3.getKey();
					if (t1 == t2 /* || t2.getState() == State.TERMINATED */)
						continue;
					for (Map.Entry<Instruction, List<MemoryAccess>> entry4 : entry3
							.getValue().entrySet()) {
						Instruction insn2 = entry4.getKey();
						// TODO: ignoring write-write conflicts
						// changed by jpso
						// if (YoshiListener.isWrite(insn2.getByteCode()))
						// continue;

						// check locks!
						List<MemoryAccess> writeLocks = entry2.getValue();
						List<MemoryAccess> readLocks = entry4.getValue();
						if (isUnprotected(writeLocks, readLocks)) {
							addIfNew(
									result,
									new Pair(
											new Pair(t1, insn1.getMethodInfo()),
											new Pair(t2, insn2.getMethodInfo())));
						}
					}
				}
			}
		}
	}

	@SuppressWarnings({ "rawtypes", "unchecked" })
	public void filterPotentialRaceList(
			List<Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>>> result) {
		for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry1 : accessMap
				.entrySet()) {
			ThreadInfo t1 = entry1.getKey();
			for (Map.Entry<Instruction, List<MemoryAccess>> entry2 : entry1
					.getValue().entrySet()) {
				Instruction insn1 = entry2.getKey();
				if (!RabbitListener.isWrite(insn1.getByteCode()))
					continue;
				for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry3 : accessMap
						.entrySet()) {
					ThreadInfo t2 = entry3.getKey();
					if (t1 == t2 /* || t2.getState() == State.TERMINATED */)
						continue;
					for (Map.Entry<Instruction, List<MemoryAccess>> entry4 : entry3
							.getValue().entrySet()) {
						Instruction insn2 = entry4.getKey();
						// TODO: ignoring write-write conflicts
						if (RabbitListener.isWrite(insn2.getByteCode()))
							continue;
						// check locks!
						List<MemoryAccess> writeLocks = entry2.getValue();
						List<MemoryAccess> readLocks = entry4.getValue();
						if (isUnprotected(writeLocks, readLocks)) {
							addIfNew(
									result,
									new Pair(
											new Pair(t1, insn1.getMethodInfo()),
											new Pair(t2, insn2.getMethodInfo())),
									(FieldInstruction) insn1);
						}
					}
				}
			}
		}
	}

	@SuppressWarnings({ "rawtypes", "unchecked" })
	public void updatePotentialRacesListInstruction(
			List<Pair<Pair<ThreadInfo, Instruction>, Pair<ThreadInfo, Instruction>>> result) {
		// Set<ThreadInfo> visited = new TreeSet<ThreadInfo>();
		for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry1 : accessMap
				.entrySet()) {
			ThreadInfo t1 = entry1.getKey();
			// if (t1.getState() == State.TERMINATED) continue;
			for (Map.Entry<Instruction, List<MemoryAccess>> entry2 : entry1
					.getValue().entrySet()) {
				Instruction insn1 = entry2.getKey();
				if (!RabbitListener.isWrite(insn1.getByteCode()))
					continue;
				for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry3 : accessMap
						.entrySet()) {
					ThreadInfo t2 = entry3.getKey();
					if (t1 == t2 /* || t2.getState() == State.TERMINATED */)
						continue;
					for (Map.Entry<Instruction, List<MemoryAccess>> entry4 : entry3
							.getValue().entrySet()) {
						Instruction insn2 = entry4.getKey();
						// TODO: ignoring write-write conflicts
						if (RabbitListener.isWrite(insn2.getByteCode()))
							continue;
						// check locks!
						List<MemoryAccess> writeLocks = entry2.getValue();
						List<MemoryAccess> readLocks = entry4.getValue();
						if (isUnprotected(writeLocks, readLocks)) {
							addIfNewInstruction(result, new Pair(new Pair(t1,
									insn1), new Pair(t2, insn2)));
						}
					}
				}
			}
		}
	}

	private void addIfNew(
			List<Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>>> result,
			Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>> pair,
			FieldInstruction insn) {
		for (Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>> p : result) {
			if (p._2._1._1 == pair._1._1 && p._2._1._2 == pair._1._2
					&& p._2._2._1 == pair._2._1 && p._2._2._2 == pair._2._2) {
				return;
			}
			if (p._2._1._1 == pair._2._1 && p._2._1._2 == pair._2._2
					&& p._2._2._1 == pair._1._1 && p._2._2._2 == pair._1._2) {
				return;
			}
		}

		Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>> newPair = new Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>>(
				insn, pair);
		result.add(newPair);
	}

	private void addIfNew(
			List<Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>> result,
			Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>> pair) {
		for (Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>> p : result) {
			if (p._1._1 == pair._1._1 && p._1._2 == pair._1._2
					&& p._2._1 == pair._2._1 && p._2._2 == pair._2._2) {
				return;
			}
			if (p._1._1 == pair._2._1 && p._1._2 == pair._2._2
					&& p._2._1 == pair._1._1 && p._2._2 == pair._1._2) {
				return;
			}
		}
		result.add(pair);
	}

	private void addIfNewInstruction(
			List<Pair<Pair<ThreadInfo, Instruction>, Pair<ThreadInfo, Instruction>>> result,
			Pair<Pair<ThreadInfo, Instruction>, Pair<ThreadInfo, Instruction>> pair) {
		for (Pair<Pair<ThreadInfo, Instruction>, Pair<ThreadInfo, Instruction>> p : result) {
			if (p._1._1 == pair._1._1 && p._1._2 == pair._1._2
					&& p._2._1 == pair._2._1 && p._2._2 == pair._2._2) {
				return;
			}
			if (p._1._1 == pair._2._1 && p._1._2 == pair._2._2
					&& p._2._1 == pair._1._1 && p._2._2 == pair._1._2) {
				return;
			}
		}
		result.add(pair);
	}

	@SuppressWarnings("unchecked")
	private boolean isUnprotected(List<MemoryAccess> writeLocks,
			List<MemoryAccess> readLocks) {
		boolean result = false;
		a: for (MemoryAccess wsei : writeLocks) {
			for (MemoryAccess rsei : readLocks) {
				if (wsei.lockSet.isEmpty() || rsei.lockSet.isEmpty()) {
					result = true;
					break a;
				}
				Set<ElementInfo> clone = ((Set<ElementInfo>) ((TreeSet<ElementInfo>) wsei.lockSet)
						.clone());
				clone.retainAll(rsei.lockSet);
				if (clone.isEmpty()) {
					/************************************
					 * both sets were originally non-empty and they do not have
					 * any monitor in common (intersection is empty). problem!
					 ************************************/
					result = true;
					break a;
				}

			}
		}
		return result;
	}

	private String printMap(Map.Entry<Instruction, List<MemoryAccess>> map) {
		StringBuilder sb = new StringBuilder();
		Instruction insn = map.getKey();
		int opcode = insn.getByteCode();
		String msg2 = (opcode == RabbitConfig.PUTFIELD_opcode) ? "WRITE"
				: (opcode == RabbitConfig.PUTSTATIC_opcode) ? "WRITE" : "READ";

		sb.append("      instruction: ");
		sb.append(insn.getSourceLocation());
		sb.append(" ");
		sb.append(msg2);
		sb.append(" ");

		sb.append(" [");
		List<MemoryAccess> set = map.getValue();
		Set<ElementInfo> monitors = new TreeSet<ElementInfo>(RabbitConfig.comp);
		for (MemoryAccess sei : set) {
			monitors.addAll(sei.lockSet);
			int i = 0, size = sei.lockSet.size();
			sb.append("(");
			for (ElementInfo ei : sei.lockSet) {
				i++;
				sb.append(ei.getIndex());
				if (i < size) {
					sb.append(", ");
				}
			}
			sb.append(")");
		}
		sb.append("] \n");
		// // sb.append("============================\n");
		// for (ElementInfo ei : monitors) {
		// sb.append("monitor id ");
		// sb.append(ei.getIndex());
		// sb.append(" ");
		// sb.append(ei.getClassInfo().getName());
		// sb.append("\n");
		// }

		return sb.toString();
	}

}